C++: Support reasoning about whether a phi node overwrites the entire buffer by MathiasVP · Pull Request #21836 · github/codeql

MathiasVP · 2026-05-12T10:59:17Z

This PR is a combination of two fixes with the overarching theme of computing which SSA definitions are certain (which, in this context, means "overwrites the entire buffer").

A brief reminder of what we use "certain" vs. "uncertain" SSA writes for: In order to model flow through something like

p[i] = source();
p[j] = 0;
sink(p[k]);

(without knowing the concrete values for i, j, and k) we model the write to p[i] and p[j] as "uncertain" writes. That is, the write to the underlying SSA variable isn't overwritten. So whatever value was previously tracked by SSA is not killed by the SSA definition.

The first improvement is in 8585bb6 which changes some of the SSA writes to be certain (whereas before they were only certain if the address they were writing to didn't involve pointer arithmetic).
The next change is slightly less well-motivated. This change is most likely necessary if we ever want to switch the instantiation of the shared range analysis library over from the sound IR-based SSA to dataflow-based SSA.

On main we currently consider any definition from a PhiNode to be an uncertain definition. This PR changes this so that we consider a PhiNode to be a certain definition whenever its inputs are all certain definitions.

There are some technical things that make this slightly more complicated than what you would expect: Since a PhNode can be its own input we need recursion over a graph with cycles, and because of QL's least fixed-point semantics we don't get the right result when doing recursion over a graph with cycles. So we instead recurse over a graph whose nodes are the the recursive PhiNodes.

As always, recursion through forall is also dangerous and should ideally be rewritten using explicit recursion over integers to reduce the risk of performance problems. However, I'll delay that until we actually see a performance problem on a database.

(I expect this work to be necessary for switching the instantiation of the shared range analysis library over to dataflow-based SSA because I expect the relevant SSA variables for range analysis to be those for which any SSA definition is a certain SSA definition.)

DCA shows a couple of lost results. They're all FPs of the form added in 8e25240 (which this PR fixes) 🎉

…itialized instructions.

…ntire buffer is overwritten).

…ics.

Copilot

Pull request overview

Updates the C++ IR-based SSA/dataflow implementation to better classify SSA definitions as “certain” (overwrites the entire buffer), including propagating certainty through PhiNodes, and adjusts/extends tests to cover the new behavior.

Changes:

Refines write-certainty tracking by replacing a boolean “certain” flag with a Certainty type and updating write handling accordingly.
Changes PhiNode certainty so phi definitions can be “certain” when their inputs are certain, including SCC-based handling for phi cycles.
Updates existing dataflow test expectations and adds a new inline-expectations test suite for “certain/uncertain” SSA definitions.

Show a summary per file

File	Description
cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImplCommon.qll	Introduces `Certainty`-typed write certainty and updates write classification logic.
cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImpl.qll	Adjusts SSA source-variable stringification and implements phi-node certainty propagation (incl. cycle handling).
cpp/ql/test/library-tests/dataflow/dataflow-tests/test.cpp	Adds a regression test case exercising behavior around certainty/uninitialized flow in a loop.
cpp/ql/test/library-tests/dataflow/certain/test.ql	Adds an inline expectations harness to assert `Ssa::Definition.isCertain()` outcomes.
cpp/ql/test/library-tests/dataflow/certain/test.cpp	Adds C++ scenarios to validate “certain vs uncertain” SSA defs and phi behavior.
cpp/ql/test/library-tests/dataflow/certain/test.expected	Empty expected file for the new inline expectations test.
cpp/ql/test/library-tests/dataflow/dataflow-tests/uninitialized.expected	Updates expected results for uninitialized/dataflow tests.
cpp/ql/test/library-tests/dataflow/dataflow-tests/test-source-sink.expected	Updates expected source-to-sink flow results.
cpp/ql/test/library-tests/dataflow/dataflow-tests/localFlow-ir.expected	Updates expected IR local flow output (notably SSA phi read formatting).
cpp/ql/test/library-tests/dataflow/dataflow-tests/dataflow-consistency.expected	Updates expected dataflow consistency outputs.
cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/constant-size/ConstantSizeArrayOffByOne.expected	Updates experimental query-test expectations to match new flow behavior.

Copilot's findings

Files reviewed: 10/11 changed files
Comments generated: 3

Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>

aschackmull · 2026-05-19T07:09:10Z

On main we currently consider any definition from a PhiNode to be an uncertain definition. This PR changes this so that we consider a PhiNode to be a certain definition whenever its inputs are all certain definitions.

Please elaborate on this. As-is this makes no sense to me, since I would not consider "certainness" to be a meaningful property of phi nodes.

aschackmull · 2026-05-19T07:16:32Z

+      if ind = 0
+      then result = "&" + base.toString()
+      else result = repeatStars(this.getIndirection() - 1) + base.toString()


Mixing direct field access ind with this.getIndirection() becomes very confusing to read. Same issue below.

Fixed in d93de54

aschackmull · 2026-05-19T07:34:17Z

+private predicate hasAnInput(PhiNode phi1, PhiNode phi2) {
+  definitionCycle(phi1) and
+  definitionCycle(phi2) and
+  getAnInput(phi1) = phi2
+}


This is wrong. You're attempting to define SCC-internal edges here, but if two SCCs are adjacent then this will accidentally merge them. You need this instead:

private predicate sccEdge(PhiNode phi1, PhiNode phi2) { getAnInput(phi1) = phi2 and getAnInput+(phi2) = phi1 }

Hm, yes I can see how these two definitions aren't equivalent and that yours captures what I intended to capture. Now I'm just trying to construct an example where the two definitions would cause a change in a test 🤔

If you have one at hand I'd love to know. Otherwise I'll spend some time trying to construct one, and if all else fail I'll just replace the code with your suggestion as it's obviously the right one

Something like this perhaps:

while (..) { // phi_1 if (..) x = .. // phi_2 } while (..) { // phi_3 if (..) x = .. // phi_4 }

Here phi_1 + phi_2 ought to form one SCC and phi_3 + phi_4 another, and your code would conflate them. I think if you make the assignment in the first loop certain, and the one in the second uncertain then you should end up with an observable difference.

That indeed did the trick. f77d426 adds the test and f5113b1 fixes it using your definition. Thanks!

aschackmull · 2026-05-19T07:40:43Z

+    forex(PhiNode phi | phi = this.getAPhiNode() |
+      forall(PhiNode inp | phi.getAnInput() = inp and not this.hasPhiNode(inp) | inp.isCertain())
+    )


Factor out the range to make the recursion simpler. Add a member predicate

pragma[nomagic] Definition getAnInput() { result = this.getAPhiNode().getAnInput() and not this.hasPhiNode(result) }

and use this to define the recursive forall:

forex(Definition inp | this.getAnInput() | inp.isCertain())

Note also that I've changed the type of inp from PhiNode to Definition - I believe that was also wrong in your version.

Fixed in c6ce13a

MathiasVP · 2026-05-19T11:12:44Z

Thanks for the comments, Schack!

Please elaborate on this. As-is this makes no sense to me, since I would not consider "certainness" to be a meaningful property of phi nodes.

Forget the "certainness" naming for the moment and just consider it to be a property of whether an SSA definition overwrites the entire buffer pointed to. For example:

void f(int* p) {
  if(b) {
    *(p + 1) = 1; // (1)
  } else {
    *(p + 1) = 2; // (2)
  }
  // (3)
}

we don't know how large the buffer pointed to by p is so the definitions at (1) and (2) are uncertain. Thus, we don't know whether the phi for *p at (3) overwrites the entire buffer pointed to by p.

Does that make things more clear?

aschackmull · 2026-05-19T11:27:48Z

Does that make things more clear?

Sort of, yes. But I still think the concept is flawed. Firstly, a phi is not a write - and if you do think of it as a write in the sense x_3 = phi(x_1, x_2) then I'd say that it always overwrites the entire buffer by definition. In your example, I'd say that the phi at (3) is fully defined by its SSA inputs from (1) and (2), so I'd always consider it to be "certain". Now those two prior definitions are themselves uncertain, so they're in turn defined by a combination of the RHS and the prior SSA definition (the init at entry). So an uncertain write is sort of like a certain write plus a phi node all wrapped into one SSA def.

MathiasVP · 2026-05-19T12:04:25Z

So an uncertain write is sort of like a certain write plus a phi node all wrapped into one SSA def.

That's also a perfectly good way one could model it, yes. In fact, I think that's exactly what is captured by a Chi instruction which we don't use in dataflow because it's based on the IR's way-too-imprecise-to-be-useful-in-dataflow memory SSA.

Anyway, obviously this is not a direction I think we should go in for this PR, but I appreciate the comments.

…the definition to be a 'PhiNode'.

github-actions Bot added the C++ label May 12, 2026

MathiasVP added no-change-note-required This PR does not need a change note and removed C++ labels May 12, 2026

github-actions Bot added the C++ label May 12, 2026

MathiasVP added 8 commits May 13, 2026 13:07

C++: Add a FP caused by missing certainty around SSA writes from Unin…

8e25240

…itialized instructions.

C++: Make 'toString' on 'Ssa::Definition' more clear.

b753e7d

C++: Add a new test to test assignment certainty (i.e., whether the e…

e77d85f

…ntire buffer is overwritten).

C++: Add missing overrides.

6d5d57a

C++: Slightly refactor certainty computation with a newtype.

fc80a24

C++: Some writes are always certain regardless of the address.

8585bb6

C++: Perform an SCC reduction to simulate greatest fixed-point semant…

f40d42c

…ics.

C++: Accept test changes in experimental query.

07b8d7e

MathiasVP force-pushed the uncertain-def-more-complete branch from 0df8ed9 to 07b8d7e Compare May 13, 2026 12:15

MathiasVP marked this pull request as ready for review May 13, 2026 12:22

MathiasVP requested a review from a team as a code owner May 13, 2026 12:22

Copilot AI review requested due to automatic review settings May 13, 2026 12:22

Copilot started reviewing on behalf of MathiasVP May 13, 2026 12:23 View session

Copilot AI reviewed May 13, 2026

View reviewed changes

Comment thread cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImplCommon.qll

Comment thread cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImpl.qll Outdated

Comment thread cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImpl.qll

Potential fix for pull request finding

25c4d9d

Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>

aschackmull reviewed May 19, 2026

View reviewed changes

C++: Consistent use of 'this.getIndirection()' in 'toString'.

d93de54

MathiasVP added 3 commits May 19, 2026 15:27

C++: Simplify recursion in 'PhiCycle::isCertain' and do not restrict …

c6ce13a

…the definition to be a 'PhiNode'.

C++: Add test demonstrating broken phi cycle certain'ness.

f77d426

C++: Fix internal SCC edges and accept test changes.

f5113b1

Conversation

MathiasVP commented May 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Copilot's findings

Uh oh!

Uh oh!

Uh oh!

Uh oh!

aschackmull commented May 19, 2026

Uh oh!

aschackmull May 19, 2026

Choose a reason for hiding this comment

Uh oh!

MathiasVP May 19, 2026

Choose a reason for hiding this comment

Uh oh!

aschackmull May 19, 2026

Choose a reason for hiding this comment

Uh oh!

MathiasVP May 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

aschackmull May 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

MathiasVP May 19, 2026

Choose a reason for hiding this comment

Uh oh!

aschackmull May 19, 2026

Choose a reason for hiding this comment

Uh oh!

MathiasVP May 19, 2026

Choose a reason for hiding this comment

Uh oh!

MathiasVP commented May 19, 2026

Uh oh!

aschackmull commented May 19, 2026

Uh oh!

MathiasVP commented May 19, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

MathiasVP commented May 12, 2026 •

edited

Loading

MathiasVP May 19, 2026 •

edited

Loading

aschackmull May 19, 2026 •

edited

Loading